<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>MinProofWorkStmt</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="MinProofWorkStmt";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/gmff/MinProofWorksheet.html" title="class in mmj.gmff"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/gmff/ModelAExporter.html" title="class in mmj.gmff"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/gmff/MinProofWorkStmt.html" target="_top">Frames</a></li>
<li><a href="MinProofWorkStmt.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.gmff</div>
<h2 title="Class MinProofWorkStmt" class="title">Class MinProofWorkStmt</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.gmff.MinProofWorkStmt</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<dl>
<dt>Direct Known Subclasses:</dt>
<dd><a href="../../mmj/gmff/MinCommentStmt.html" title="class in mmj.gmff">MinCommentStmt</a>, <a href="../../mmj/gmff/MinDistinctVariablesStmt.html" title="class in mmj.gmff">MinDistinctVariablesStmt</a>, <a href="../../mmj/gmff/MinFooterStmt.html" title="class in mmj.gmff">MinFooterStmt</a>, <a href="../../mmj/gmff/MinGeneratedProofStmt.html" title="class in mmj.gmff">MinGeneratedProofStmt</a>, <a href="../../mmj/gmff/MinHeaderStmt.html" title="class in mmj.gmff">MinHeaderStmt</a>, <a href="../../mmj/gmff/MinProofStepStmt.html" title="class in mmj.gmff">MinProofStepStmt</a></dd>
</dl>
<hr>
<br>
<pre>public abstract class <span class="strong">MinProofWorkStmt</span>
extends java.lang.Object</pre>
<div class="block">General object representing a statement in a MinProofWorksheet.</div>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/gmff/MinProofWorkStmt.html#MinProofWorkStmt(mmj.gmff.MinProofWorksheet, java.lang.String[][])">MinProofWorkStmt</a></strong>(<a href="../../mmj/gmff/MinProofWorksheet.html" title="class in mmj.gmff">MinProofWorksheet</a>&nbsp;w,
                java.lang.String[][]&nbsp;slc)</code>
<div class="block">Standard MinProofWorkStmt constructor.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>abstract void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/MinProofWorkStmt.html#buildModelAExport(mmj.gmff.GMFFExporter, java.lang.StringBuilder)">buildModelAExport</a></strong>(<a href="../../mmj/gmff/GMFFExporter.html" title="class in mmj.gmff">GMFFExporter</a>&nbsp;gmffExporter,
                 java.lang.StringBuilder&nbsp;exportBuffer)</code>
<div class="block">Formats export data for the Proof Worksheet statement according to the
 <code>Model A</code> specifications and loads the data into a specified
 buffer.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>static <a href="../../mmj/gmff/MinProofWorkStmt.html" title="class in mmj.gmff">MinProofWorkStmt</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/MinProofWorkStmt.html#constructStmt(mmj.gmff.MinProofWorksheet, java.util.List)">constructStmt</a></strong>(<a href="../../mmj/gmff/MinProofWorksheet.html" title="class in mmj.gmff">MinProofWorksheet</a>&nbsp;minProofWorksheet,
             java.util.List&lt;java.util.List&lt;java.lang.String&gt;&gt;&nbsp;lineList)</code>
<div class="block"><code>constructStmt</code> builds a <code>MinProofWorkStmt</code> from an List of
 an List of String chunks which are either Metamath whitespace or Metamath
 tokens.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/MinProofWorkStmt.html#getCleanedLineString(int)">getCleanedLineString</a></strong>(int&nbsp;lineIndex)</code>
<div class="block">Converts whitespace chunks in line of the <code>MinProofWorkStmt</code> to
 spaces.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/MinProofWorkStmt.html#getCleanedLineString(int, int, int)">getCleanedLineString</a></strong>(int&nbsp;lineIndex,
                    int&nbsp;fromChunkIndex,
                    int&nbsp;toChunkIndex)</code>
<div class="block">Converts whitespace chunks in part of a line of the
 <code>MinProofWorkStmt</code> to spaces.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>protected boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/MinProofWorkStmt.html#isChunkWhitespace(java.lang.String)">isChunkWhitespace</a></strong>(java.lang.String&nbsp;s)</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/MinProofWorkStmt.html#typesetFormulaSymbols(mmj.gmff.GMFFExporter, java.lang.StringBuilder, java.lang.String[], int)">typesetFormulaSymbols</a></strong>(<a href="../../mmj/gmff/GMFFExporter.html" title="class in mmj.gmff">GMFFExporter</a>&nbsp;gmffExporter,
                     java.lang.StringBuilder&nbsp;exportBuffer,
                     java.lang.String[]&nbsp;lineChunks,
                     int&nbsp;startOfFormulaSymbols)</code>
<div class="block">Utility function to typeset and reformat a portion of a <code>String</code>
 array containing Metamath tokens representing at least a portion of a
 formula.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="MinProofWorkStmt(mmj.gmff.MinProofWorksheet, java.lang.String[][])">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>MinProofWorkStmt</h4>
<pre>public&nbsp;MinProofWorkStmt(<a href="../../mmj/gmff/MinProofWorksheet.html" title="class in mmj.gmff">MinProofWorksheet</a>&nbsp;w,
                java.lang.String[][]&nbsp;slc)</pre>
<div class="block">Standard MinProofWorkStmt constructor.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>w</code> - <code>MinProofWorksheet</code> of which this statement is a part.</dd><dd><code>slc</code> - Array of Array of String representing the lines and "chunks"
            making up the <code>MinProofWorkStmt</code>.</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="constructStmt(mmj.gmff.MinProofWorksheet, java.util.List)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>constructStmt</h4>
<pre>public static&nbsp;<a href="../../mmj/gmff/MinProofWorkStmt.html" title="class in mmj.gmff">MinProofWorkStmt</a>&nbsp;constructStmt(<a href="../../mmj/gmff/MinProofWorksheet.html" title="class in mmj.gmff">MinProofWorksheet</a>&nbsp;minProofWorksheet,
                             java.util.List&lt;java.util.List&lt;java.lang.String&gt;&gt;&nbsp;lineList)</pre>
<div class="block"><code>constructStmt</code> builds a <code>MinProofWorkStmt</code> from an List of
 an List of String chunks which are either Metamath whitespace or Metamath
 tokens.
 <p>
 The first line of a statement identifies the type of Proof Worksheet
 statement. <code>constructStmt</code> validates those simply in order to be
 able to determine which type of Proof Worksheet statement must be
 constructed. In addition it checks to see if the starting portion--up to
 theorem label-- is valid, and then it extracts the theorem label and
 stores it in the input minProofWorksheet object. <b> Errors result in
 accum'ing of error message(s) in the <code>Messages</code> as well as setting
 of <code>structuralError</code> in the input <code>MinProofWorksheet</code> object.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>minProofWorksheet</code> - GMFF version of <code>ProofWorksheet</code></dd><dd><code>lineList</code> - List of List of String chunks representing the text of a
            <code>ProofWorksheet</code> broken into Metamath whitespace and
            tokens grouped by line of the <code>ProofWorksheet</code>.</dd>
<dt><span class="strong">Returns:</span></dt><dd>MinProofWorkStmt returns a specific type of
         <code>MinProofWorkStmt</code> according to the first token of the
         first line of the statement text.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.lang.IllegalArgumentException</code> - if lineList is empty or if the first
             line has no <code>String</code> chunks.</dd></dl>
</li>
</ul>
<a name="buildModelAExport(mmj.gmff.GMFFExporter, java.lang.StringBuilder)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>buildModelAExport</h4>
<pre>public abstract&nbsp;void&nbsp;buildModelAExport(<a href="../../mmj/gmff/GMFFExporter.html" title="class in mmj.gmff">GMFFExporter</a>&nbsp;gmffExporter,
                     java.lang.StringBuilder&nbsp;exportBuffer)
                                throws <a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></pre>
<div class="block">Formats export data for the Proof Worksheet statement according to the
 <code>Model A</code> specifications and loads the data into a specified
 buffer.
 <p>
 Export data is based on model files which vary according to the Model Id
 and Proof Worksheet statement type. In general, model files contain
 fragments of export data, such as html fragments -- but a model file may
 also represent a placeholder for insertion of formatted text from the
 Proof Worksheet. Model files are also categorized as Required or
 Optional. Required model files, if not found when read by the program
 trigger an error message and prevent export of the entire proof. Optional
 model files if not found when read simply prevent export of part of the
 proof -- for example, Comments -- and no error messages are generated.
 Placeholder model files, whether Required or Optional, which exist but
 contain no data indicate to the program that proof text is not to be
 output at this location in the export text.
 <p>
 Additional information may be found \GMFFDoc\GMFFModels.txt.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>gmffExporter</code> - The <code>GMFFExporter</code> requesting the export data
            build.</dd><dd><code>exportBuffer</code> - The <code>StringBuilder</code> to which exported data is
            to be output.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></code> - if errors are encountered during the export
             process.</dd></dl>
</li>
</ul>
<a name="typesetFormulaSymbols(mmj.gmff.GMFFExporter, java.lang.StringBuilder, java.lang.String[], int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>typesetFormulaSymbols</h4>
<pre>public&nbsp;void&nbsp;typesetFormulaSymbols(<a href="../../mmj/gmff/GMFFExporter.html" title="class in mmj.gmff">GMFFExporter</a>&nbsp;gmffExporter,
                         java.lang.StringBuilder&nbsp;exportBuffer,
                         java.lang.String[]&nbsp;lineChunks,
                         int&nbsp;startOfFormulaSymbols)</pre>
<div class="block">Utility function to typeset and reformat a portion of a <code>String</code>
 array containing Metamath tokens representing at least a portion of a
 formula.
 <p>
 There are two types of "chunks" to be typeset: whitespace chunks and
 non-whitespace chunks. Non-whitespace chunks are presumed to be Metamath
 ASCII symbols which are converted into export data (e.g. html) using the
 Metamath $t comment statement data. Whitespace chunks are cleaned so that
 they contain only spaces, and in addition, are shortened by one character
 for readability.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>gmffExporter</code> - The <code>GMFFExporter</code> requesting the export data
            build.</dd><dd><code>exportBuffer</code> - The <code>StringBuilder</code> to which exported data is
            to be output.</dd><dd><code>lineChunks</code> - <code>String</code> array containing Metamath tokens or
            whitespace.</dd><dd><code>startOfFormulaSymbols</code> - index into <code>lineChunks</code> indicating the
            beginning of the typesetting operation (which proceeds through
            the end of the array -- effectively we are just bypassing an
            initial part of the array.)</dd></dl>
</li>
</ul>
<a name="getCleanedLineString(int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getCleanedLineString</h4>
<pre>public&nbsp;java.lang.String&nbsp;getCleanedLineString(int&nbsp;lineIndex)</pre>
<div class="block">Converts whitespace chunks in line of the <code>MinProofWorkStmt</code> to
 spaces.
 <p>
 By the time a Proof Worksheet statement gets to this part of the code,
 the only non-space whitespace character is Tab -- and on the Proof
 Assistant GUI Tab characters equate to one space. To be really safe, all
 whitespace chunk characters are converted to spaces.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>lineIndex</code> - index of line in <code>stmtLineChunks</code> to be "cleaned".</dd>
<dt><span class="strong">Returns:</span></dt><dd>String containing all chunks in the line concatenated with
         whitespace chunks converted to spaces.</dd></dl>
</li>
</ul>
<a name="getCleanedLineString(int, int, int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getCleanedLineString</h4>
<pre>public&nbsp;java.lang.String&nbsp;getCleanedLineString(int&nbsp;lineIndex,
                                    int&nbsp;fromChunkIndex,
                                    int&nbsp;toChunkIndex)</pre>
<div class="block">Converts whitespace chunks in part of a line of the
 <code>MinProofWorkStmt</code> to spaces.
 <p>
 By the time a Proof Worksheet statement gets to this part of the code,
 the only non-space whitespace character is Tab -- and on the Proof
 Assistant GUI Tab characters equate to one space. To be really safe, all
 whitespace chunk characters are converted to spaces.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>lineIndex</code> - index of line in <code>stmtLineChunks</code> to be "cleaned".</dd><dd><code>fromChunkIndex</code> - index of first chunk in the line to be "cleaned".</dd><dd><code>toChunkIndex</code> - exclusive endpoint (i.e. not thru) of chunk cleanup
            operation :-)</dd>
<dt><span class="strong">Returns:</span></dt><dd>String containing all designated chunks in the line concatenated
         with whitespace chunks converted to spaces.</dd></dl>
</li>
</ul>
<a name="isChunkWhitespace(java.lang.String)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>isChunkWhitespace</h4>
<pre>protected&nbsp;boolean&nbsp;isChunkWhitespace(java.lang.String&nbsp;s)</pre>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/gmff/MinProofWorksheet.html" title="class in mmj.gmff"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/gmff/ModelAExporter.html" title="class in mmj.gmff"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/gmff/MinProofWorkStmt.html" target="_top">Frames</a></li>
<li><a href="MinProofWorkStmt.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
